M1, M2:MsgA.
M1  M2
 (k:Knd, x:Id, s:M2.state, v:M2.da(k), w:(M2.ds(x)).
 M2.ef(k,x,s,v,w)  M1.ef(k,x,s,v,w)) 

latex

Definitions	<a, b>, M.ef(k,x,s,v,w), M.ds(x), M.da(a), M.state, M1  M2, MsgA, Valtype(da;k), P & Q, z != f(x)  P(a;z), b, x  dom(f), f(x), product-deq(A;B;a;b), a:A fp B(a), State(ds), KindDeq, t.1, IdLnk, f  g, A c B, x:A  B(x), f(a), , s = t, suptype(S; T), , P  Q, S  T, x:AB(x), t.2, x. t(x), x.A(x), Knd, Top, f(x)?z, Void, Type, x:A. B(x), Id, IdDeq, t  T
Lemmas	id-deq wf, Id wf, fpf-cap-void-subtype, Knd wf, pi2 wf, fpf-cap wf, top wf, subtype-fpf-cap-top, rationals wf, pi1 wf, Kind-deq wf, ma-state wf, fpf-trivial-subtype-top, product-deq wf, fpf-ap wf, fpf-dom wf, assert wf, ma-ds wf, ma-da wf, ma-st wf, ma-sub wf, msga wf